プログラム意味論(本, 横内)

#プログラム意味論

chapt. 1

表示的意味論

結論としては$ \cal{M}_{exp}と$ \cal{M}_{cmd}といった意味関数（解釈関数）を定義したり，吟味したりするという

操作的意味論

もっとハード的に寄り添い，この操作をするとレジスタの値とかがどうなるのか？を回路として埋め込んでおけば，それで意味が発生する

chapt2.

関数の名前とかは一旦捨象して計算そのものに目を向ける

$ \lambda x.x+1

$ (\lambda x.x+1)(2)

仮引数（上の例だと$ x）を$ 2に置き換える操作のことをさす

Curry化

$ f(x,y) = x + y

$ \lambda x. (\lambda y. x + y)

一般に$ n引数関数$ f(x_1 \cdots x_n)は

$ \lambda x_1. (\lambda x_2. ( \cdots (\lambda x_n. f(x_1 \cdots x_n)) \cdots ))と書き表される

まず，型無しλ計算をやる

ラムダ計算についての形式的定義

自由変数（自由変項）がないラムダ式をコンビネータと呼ぶ

つまり，ラムダ式$ Mについて$ fv(M) = \empty

chapt3.

近似

適当な二項関係，半順序$ \sqsubseteq

反射律：$ a \sqsubseteq a

反対称的：$ a \sqsubseteq b \land b \sqsubseteq a \implies a = b

推移律：$ a \sqsubseteq b \land b \sqsubseteq c \implies a \sqsubseteq c

最小元，最大元

半順序集合$ Dの最小元$ \botとは$ \forall a \in D . (\bot \sqsubseteq a)

半順序集合が必ず最小元を持つとは限らない

もちろん最大元$ \topがあって$ \forall a \in D.(a \sqsubseteq \top)

最小限，最大限は存在しないか，存在すれば唯一

また$ Dを強調して$ \bot_D,\top_Dと書く

上界，上限，下界，下限

$ D, X \sub D, d \in Dについて

$ \forall x \in X. (x \sqsubseteq d)なら$ dを$ Xの上限

特に，$ dが$ Xの最小元なら$ dは$ Xの上限

$ \forall x \in X. (d \sqsubseteq x)なら$ dを$ Xの下界

特に，$ dが$ Xの最大元なら$ dは$ Xの下限

$ Xの上限，下限は存在しないか，唯一だけ存在する，それぞれ$ \sqcup X, \sqcap Xとする

完備束

半順序集合$ Dの任意の部分集合$ X \sub Dに対して上限が存在するなら，$ Dを完備束と呼ぶ

$ \forall X \sub D. \exists m \in D. m = \sqcup X

定義より

$ X = \empty \implies \sqcup X = \bot_D

$ X = D \implies \sqcup X = \top_D

ωチェーン：半順序集合$ Dの元の列$ a_0 \sqsubseteq a_1 \sqsubseteq a_2 \sqsubseteq \cdots

緩めたバージョン，有向集合

半順序集合$ Dの空でない部分集合$ Xについて

$ \forall a,b,c \in X. (a \sqsubseteq c \land b \sqsubseteq c)

完備半順序集合$ D，cpo

$ Dは最小限$ \bot_Dを持つ

$ Dの任意の有向部分集合$ Xについて，$ Xの上限$ \sqcup X \in Dが存在する